module Lexer(Token(..), WordRsv(..), TknPOCTL(..), ProLOp(..), TempOp(..), lexer, lexerPOCTL) where

import Data.Char

-- Aliases of some primitive types
type Atom   = String
type Obser  = [Char]
type States = Int

-- Datatype for the tokens in which the HMM is broken into
data Token = SetSt States
             | SetObs Obser
             | Rsv WordRsv
             | ODef
             | Lista [Float]
             | ListFloat [Float]
             | ListAtom [[Atom]]
               deriving Show                        
                        
-- Datatype for the tokens of POCTL*
data TknPOCTL = Ttrue 
              | Ffalse 
              | AProp Atom 
              | LogOp ProLOp 
              | TempOp TempOp 
              | Comp String
              | NextObs Obser 
              | Range Float 
              | UBound Int 
              | ProbOp
              | LeftPar 
              | RightPar 
              | LeftSqBrckt
              | RightSqBrckt 
              | Underscore 
              deriving Show

-- Datatype for logical operators
data ProLOp = Neg | Conj | Disj deriving Show

-- Datatype for temporal operators
data TempOp = NextO | UntilO deriving Show

--data CompOp = Less | LessEq | Greater | GreaterEq deriving Show

-- Datatype for the tokens of reserved words
data WordRsv = St | Trans | Lbl | Obs | ObsProb | IniDist 
             deriving Show
                      
-----------------------------------------------------------------------------------
-----------------------------------------------------------------------------------
-- This function takes a string, i.e. a file with the elements of an HMM, and returns
-- the list of tokens that make up the HMM   
lexer :: String -> [Token]
lexer "" = []
lexer (c:left) | isSpace c = lexer left
lexer ('=':rmndr) = ODef : lexer rmndr

-- We're about to read a reserved word or a integer that 
-- represents the number of states
lexer (c:left) 
  | isAlpha c = lexIdRsv (c:left)
  | isDigit c = token : lexer newLeft    
  where 
    (tmp, newLeft) = break (not . isDigit) (c:left)
    token = SetSt (read tmp::Int)
    
-- We're about to read the set of observations 
lexer ('"':rmndr) = token : lexer newRmndr 
  where
    (tmp, xs) = break (=='"') rmndr
    newRmndr  = if null xs 
                then error "Unable to generate token. Problem reading the set of observations." 
                else tail xs
    token     = SetObs tmp
    
-- Now we read the labelling function
lexer ('[':'[':'"':remainder) = ListAtom lst : lexer newRemainder 
  where
    (lst, xs) = getLbls ('"':remainder)
    newRemainder = if length xs < 2 
                   then error "Unable to generate token. Problem reading the set of atomic propositions for each state." 
                   else tail (tail xs)
                        
-- This is the case where we read the matrix of float values
lexer ('[':'[':left) = ListFloat token : lexer newLeft 
  where 
    (token, xs) =  ffloats left
    newLeft = if length xs < 2 
              then error "Unable to generate token. Problem reading the matrix of float values." 
              else tail (tail xs)

-- Finally, we read the initial distribution vector of float values
lexer ('[':rmndr) = Lista (floatSimple token) : lexer newRmndr 
  where 
    (token, xs) = break (==']') rmndr
    newRmndr = if null xs 
               then error "Unable to generate token. Problem reading the initial probability values." 
               else tail xs
lexer _ = error "Unrecognizable token."  



-- This function takes a string representing a  matrix of the form ..], [..], .., [..]]
-- of float values and returns the corresponding list of list of float values
ffloats :: String -> ([Float], String)
ffloats list = if (head (tail aux2)==']') 
               then (res,aux2) 
               else (res ++ tmp1, tmp2) 
  where    
    (aux1,aux2) =  break (==']') list   
    res = ffloatList aux1
    (tmp1,tmp2) = ffloats (tail aux2)
    
-- With this functions we identify a list of floats form a string [..]
ffloatList :: String -> [Float]
ffloatList [] = []
ffloatList (',':left) = ffloatList left 
ffloatList (c:left) | isSpace c = ffloatList left
ffloatList ('[':left) = ffloatList left
ffloatList left = 
  if null sndPart 
  then (read (num1)::Float):ffloatList leftL  
  else if (head sndPart=='.') 
       then let (num2, _) = break (not . isDigit) (tail sndPart) 
            in (read (num1++"."++num2)::Float):ffloatList leftL 
       else error "Problem while reading the transition probability matrix." 
  where
    (tmp, leftL) = break (\x-> x==',') left
    (fstPart,sndPart) = break (\x-> x=='.' || not(isDigit x)) tmp
    num1 = if null fstPart
           then "0" 
           else fstPart 
    
-- This function takes a string of the form f, f,.., f] and 
-- returns the list of floats produced by it
floatSimple :: String -> [Float]
floatSimple [] = []
floatSimple (',':rmndr) = floatSimple rmndr 
floatSimple (c:rmndr) | isSpace c = floatSimple rmndr
floatSimple rmndr = 
  if null sndPart 
  then (read (num1)::Float):floatSimple rmndrL  
  else if (head sndPart=='.') 
       then let (num2, _) = break (not . isDigit) (tail sndPart) 
            in (read (num1++"."++num2)::Float):floatSimple rmndrL 
       else error "Problem while reading the initial distribution vector." 
  where
    (tmp, rmndrL) = break (\x-> x==',') rmndr
    (fstPart,sndPart) = break (\x-> x=='.' || not(isDigit x)) tmp
    num1 = if null fstPart 
           then "0" 
           else fstPart 

-- With this function we obtain the list of observations (strings) assigned to 
-- each state. 
-- Its input is a string of the form ".. ", "..", .., ".."], [".. ", "..", .., ".."], .., [".. ", "..", .., ".."]]
getLbls :: String -> ([[Atom]], String)
getLbls list = if (head (tail aux2) == ']') 
               then (res:[], aux2) 
               else (res:tmp1, tmp2) 
  where
    (aux1, aux2) = break (==']') list
    res = parseStrings aux1
    (tmp1, tmp2) = getLbls (tail aux2)

-- This auxiliary function takes a string of the form [".. ", "..", .., ".."] and returns
-- a list of strings
parseStrings :: String -> [String]
parseStrings [] = []
parseStrings (',':rmndr) = parseStrings rmndr 
parseStrings (c:rmndr) | isSpace c = parseStrings rmndr 
parseStrings ('[':rmndr) = parseStrings rmndr
parseStrings ('"':rmndr) | null myLst  = error "Problem while reading labels, no closing \" (quotation mark)"
                         | otherwise   = atom : parseStrings (tail myLst)    
  where
    (atom, myLst) = break (=='"') rmndr
parseStrings _ = error "Problem while reading labels."

-- With the next function we recognized reserved words
lexIdRsv :: String -> [Token]
lexIdRsv xs =
  let (name, left) = break (not . isAlpha) xs
      token        = case name of 
        "States"        -> Rsv St
        "Transitions"   -> Rsv Trans
        "Labelling"     -> Rsv Lbl
        "Observations"  -> Rsv Obs 
        "ObsProb"       -> Rsv ObsProb
        "Initial"       -> Rsv IniDist 
        _               -> error "No reserved word"
  in token : lexer left
     

-----------------------------------------------------------------------------------
-----------------------------------------------------------------------------------
-- This function returns a list of tokens taken out  
-- of a string representing a POCTL* formula
lexerPOCTL :: String -> [TknPOCTL]
lexerPOCTL "" = []
lexerPOCTL (c:left) | isSpace c = lexerPOCTL left
lexerPOCTL ('(':rmndr) = LeftPar  : (lexerPOCTL rmndr)
lexerPOCTL (')':rmndr) = RightPar : (lexerPOCTL rmndr)
lexerPOCTL ('[':left)  = LeftSqBrckt : (lexerPOCTL left)
lexerPOCTL (']':left)  = RightSqBrckt: (lexerPOCTL left)
lexerPOCTL ('v':left)  = LogOp Disj  : (lexerPOCTL left)
lexerPOCTL ('^':left)  = LogOp Conj  : (lexerPOCTL left)
lexerPOCTL ('~':left)  = LogOp Neg   : (lexerPOCTL left)
lexerPOCTL ('X':rmndr) = TempOp NextO : (lexerPOCTL rmndr)
lexerPOCTL ('U':rmndr) = TempOp UntilO: (lexerPOCTL rmndr)
lexerPOCTL ('T':rmndr) = Ttrue : lexerPOCTL rmndr
lexerPOCTL ('F':rmndr) = Ffalse : lexerPOCTL rmndr
lexerPOCTL ('P':rmndr) = ProbOp : lexerPOCTL rmndr
lexerPOCTL ('<':'=':left) = Comp "<=" : lexerPOCTL left
lexerPOCTL ('<':left) = Comp "<" : lexerPOCTL left
lexerPOCTL ('>':'=':left) = Comp ">=" : lexerPOCTL left
lexerPOCTL ('>':left) = Comp ">" : lexerPOCTL left
lexerPOCTL ('_':rmndr) = Underscore : lexerPOCTL rmndr
lexerPOCTL (c:rmndr) | isDigit c = lexFloatInt (c:rmndr) 
                     | isAlpha c = lexAtom (c:rmndr)
lexerPOCTL ('{':rmndr) = if null aux2
                         then error "Not closing bracket for the set of observations."
                         else NextObs aux1 : (lexerPOCTL (tail aux2)) 
  where
    (aux1, aux2) = break (=='}') rmndr
lexerPOCTL _ = error "Unrecognizable symbol."



-- This function takes a string with a digit in its begining and
-- returns the corresponding TknPOCTL, which is either an integer  
-- that bounds the until operator (UBound n) or a float value 
-- that defined the probability range in the probability operator
lexFloatInt :: String -> [TknPOCTL]
lexFloatInt xs = if not (null aux2)
                 then if (head aux2 == '.') 
                      then let (tmp1, tmp2) = break (not . isDigit) (tail aux2) 
                           in Range (read (aux1++"."++tmp1)) : lexerPOCTL tmp2
                      else UBound (read aux1) : lexerPOCTL aux2
                 else UBound (read aux1) : lexerPOCTL aux2
  where
    (aux1, aux2) = break (not.isDigit) xs
    
-- A string that is not an operator nor a special character is 
-- an atomic proposition. This function recognizes atomic propositions.
lexAtom ys = AProp aux1 : lexerPOCTL aux2 
  where
    (aux1, aux2) = break (\x-> not(isAlpha x) || isReserved x) ys 
    
-- This function determines if it's input is a reserved symbol
isReserved :: Char -> Bool 
isReserved c = c=='v' || c=='X' || c=='U' || c=='P' || c=='T' || c=='F'